a, b, c:. 0 < c  (a < b  c * a < c * b) 

latex

Definitions	P  Q, r - s, True, T, , t  T, P  Q, P & Q, P  Q, P  Q, x:A. B(x), False, A, {T}, S  T
Lemmas	qpositive wf, assert wf, not functionality wrt iff, assert-qpositive, qminus positive, mon ident q, qadd inv assoc q, qsub wf, qmul-positive, qmul over minus qrng, qmul over plus qrng, qinverse q, qadd comm q, qmul comm qrng, true wf, squash wf, qadd preserves qless, qadd wf, iff transitivity, rationals wf, int inc rationals, qmul wf, qless wf